l:IdLnk, p:IdLnk List.
lpath(l.p)

lpath(p) & (||p|| = 0  destination(l) = source(hd(p))  Id & hd(p) = lnk-inv(l)  IdLnk) 

latex

Definitions	Dec(P), P  Q, SQType(T), {T}, tl(l), l[i], ij, i<j, T, True, {i..j}, i  j < k, AB, False, P  Q, P  Q, lpath(p), P & Q, Id, destination(l), source(l), A, Prop, hd(l), P  Q, lnk-inv(l), ||as||, ij, x:A. B(x), t  T, IdLnk
Lemmas	IdLnk wf, non neg length, lnk-inv wf, hd wf, not wf, lsrc wf, ldst wf, Id wf, length wf1, lpath wf, select cons tl, true wf, squash wf, length cons, int seg wf, decidable int equal, le wf, select wf